Inference at * 1 1 1 1 
Iof proof for Lemma ax choice:



1. A : Type
2. B : Type
3. Q : AB
4. g : x:Ay:B  Q(x,y)
5. x : A
6. y : y:B  Q(x,y)
7. y = g(x)
  Q(x,(g(x)).1) 

latex

 by D 6 

latex

 1: 

 1: 6. y1 : B
 1: 7. y2 : Q(x,y1)
 1: 8. <y1, y2> = g(x)
 1:   Q(x,(g(x)).1)
 .

Definitions

x:A  B(x)